COMMENT ⊗   VALID 00013 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	functions as lists. Two variants
C00003 00003	the approach using association lists
C00014 00004	(proof alistfacts)
C00017 00005	the approach using lists of numbers
C00019 00006	*extensionality
C00025 00007	equivalence of uniqueness and inj
C00028 00008	equivalence of uniqueness and inj
C00031 00009	unpleasant rewriting
C00036 00010	alist induction
C00038 00011	(proof alistproofs)
C00041 00012	samemap
C00042 00013	apparently stronger definition of samemap
C00047 ENDMK
C⊗;
;functions as lists. Two variants

(wipe-out)
(get-proofs nth)
;the approach using association lists
;the notion of application for association lists
(proof appalist)

(decl dom (type: |GROUND→GROUND|))
(defax dom |∀xa y alist.dom nil=nil∧
                        dom((xa.y).alist)=xa.dom alist| )
(label domdef)

(decl range (type: |GROUND→GROUND|))
(defax range |∀xa y alist.range nil=nil∧
                          range((xa.y).alist)=y.range alist| )
(label rangedef)

(decl functp (type: |GROUND→TRUTHVAL|))
(define functp |∀alist.functp(alist)≡uniqueness dom(alist)|)
(label functdef)

(decl injectp (type: |GROUND→TRUTHVAL|))
(define injectp |∀alist.injectp(alist)≡functp(alist)∧uniqueness range(alist)|)
(label injectdef)

(decl (appalist) (type: |ground⊗ground→ground|))
(define appalist |∀alist y.appalist(y,alist)=cdr assoc(y,alist)|)
(label appalistdef)

(decl (samemap) (type: |ground⊗ground→truthval|))
(define samemap 
 |∀alist alist1.samemap(alist,alist1)≡
                mklset dom(alist)=mklset dom(alist1)∧
                (∀y.yεmklset dom(alist)⊃appalist(y,alist)=appalist(y,alist1))|)
(label samemapdef)

(define permutp |∀alist.permutp(alist)≡
                        functp(alist)∧mklset(dom(alist))=mklset(range(alist))|)
(label permutp_def)

(axiom |∀chi.chi(nil)∧(∀xa y alist.chi(alist)⊃chi((xa.y).alist))⊃(∀alist.chi(alist))|)
(label alistinduction)
(proof alistfacts)

(axiom |∀alist.listp(dom alist)|)
(label domsort)(label simpinfo)

(axiom |∀alist.listp(range alist)|)
(label rangesort)(label simpinfo)

(axiom |∀alist.length (dom(alist))=length alist|)
(label domlength)

(axiom |∀alist.length(dom(alist))=length(range(alist))|)
(label domrangelength)

(axiom |∀alist y.sexp appalist(y,alist)|)
(label appalistsort)(label simpinfo)

(axiom |∀alist y.¬yεmklset(dom(alist))⊃appalist(y,alist)=nil|)
(label trivial_appalist)

    ;(axiom |∀alist z.member(z,range alist)⊃(∃x.member(x.z,alist))|)
    ;(label member_range)

    ;(axiom |∀alist x z.member(x.z,alist)⊃member(z,range(alist))|)
    ;(label membership_alist_range)

    ;(axiom |∀alist x z.x=appalist(z,alist)∧atom assoc(z,alist)⊃null x|)
    ;(label trivial_assoc)

(axiom |∀alist.samemap(alist,alist)|)
(label samemap_equivalence)

(axiom |∀alist alist1.samemap(alist,alist1)⊃samemap(alist1,alist)|)
(label samemap_equivalence)

(axiom 
   |∀alist alist1 alist2.
       samemap(alist,alist1)∧samemap(alist1,alist2)⊃samemap(alist,alist2)|)
(label samemap_equivalence)

(axiom |∀alist1 alist2.samemap(alist1,alist2)≡
                       (mklset(dom(alist1))=mklset(dom(alist2))∧
                       (∀x.appalist(x,alist1)=appalist(x,alist2)))|)
(label samemap_def1)
;the approach using lists of numbers
(proof appl)

(define appl |∀u i.appl(u,i)=nth(u,i)|)
(label appldef)

;extensionality for functions 

(axiom |∀u v.length u=length v∧(∀i.i<length u⊃appl(u,i)=appl(v,i))⊃u=v|)
(label extensionality)
 
(axiom |∀u i.i<length u ⊃ sexp(appl(u,i))∧member(appl(u,i),u)|)
(label applfacts) (label simpinfo)

;predicates for functions 

(decl (into) (type: |ground→truthval|))
(define into |∀u.into(u)=(∀n.n<length u⊃natnum nth(u,n)∧nth(u,n)<length u)|)
(label intodef)

(decl (onto) (type: |ground→truthval|))
(define onto |∀u.onto(u)=(into(u)∧(∀n.n<length u⊃member(n,u)))|)
(label ontodef)
 
(decl (perm) (type: |ground→truthval|))
(define perm |∀u.perm(u)=onto(u)|)

;equivalence of notions of uniqueness

(decl (inj) (type: |ground→truthval|))
(define inj |∀u.inj(u)=∀n m.n<length(u)∧m<length(u)∧nth(u,n)=nth(u,m)⊃n=m|)
(label injdef)

(axiom |∀u.uniqueness(u)≡inj(u)|)
(label uniqueness_injectivity)

(save-proofs appl)
;*extensionality

(proof extensionality)

(assume |length u=length v|)(label ext1)

(assume |N<LENGTH U|)(label ext2)

(assume |(∀I.I<LENGTH (NTHCDR(U,N'))⊃NTH(NTHCDR(U,N'),I)=NTH(NTHCDR(V,N'),I))⊃
         NTHCDR(U,N')=NTHCDR(V,N')|) (label ext_indhyp)

(assume |(∀I.I<LENGTH (NTHCDR(U,N'))'⊃
          NTH(NTH(U,N).NTHCDR(U,N'),I)=NTH(NTHCDR(V,N),I))|)(label ext3)

;(derive |LENGTH (NTHCDR(U,N'))=LENGTH U-N'| (length_nthcdr less_lesseqsucc ext2))

(rw ext2 (use ext1 mode: exact))
;N<LENGTH V
(label ext4)

(rw ext3 (use ext4 mode: exact)(use nthcdr_car_cdr ue: ((u.v)(n.n)) ext4 mode: exact))
(label ext5)
;∀I.I<LENGTH (NTHCDR(U,N'))'⊃
;   NTH(NTH(U,N).NTHCDR(U,N'),I)=NTH(NTH(V,N).NTHCDR(V,N'),I)


;(rw ext5 (use ext6 mode: exact) (open nth))

(ue (i |0|) * (open nth))
;NTH(U,N)=NTH(V,N)
(label ext6)

(ue (i |i'|) ext5 (open nth))
;I<LENGTH (NTHCDR(U,N'))⊃NTH(NTHCDR(U,N'),I)=NTH(NTHCDR(V,N'),I)

(derive |nthcdr(u,n')=nthcdr(v,n')| (ext_indhyp *))
 
(trw |nth(u,n).nthcdr(u,n')=nthcdr(v,n)| 
 (use nthcdr_car_cdr ue: ((u.v)(n.n)) ext4 mode: exact) (use ext6 * mode: exact))
;NTH(U,N).NTHCDR(U,N')=NTHCDR(V,N)
;deps: (EXT1 EXT2 EXT_INDHYP EXT3)

(ci ext3)
;(∀I.I<LENGTH (NTHCDR(U,N'))'⊃NTH(NTH(U,N).NTHCDR(U,N'),I)=NTH(NTHCDR(V,N),I))⊃
;NTH(U,N).NTHCDR(U,N')=NTHCDR(V,N)

(ci ext_indhyp)

(ci ext2)
;N<LENGTH U⊃
;(((∀I.I<LENGTH (NTHCDR(U,N'))⊃NTH(NTHCDR(U,N'),I)=NTH(NTHCDR(V,N'),I))⊃
;  NTHCDR(U,N')=NTHCDR(V,N'))⊃
; ((∀I.I<LENGTH (NTHCDR(U,N'))'⊃
;      NTH(NTH(U,N).NTHCDR(U,N'),I)=NTH(NTHCDR(V,N),I))⊃
;  NTH(U,N).NTHCDR(U,N')=NTHCDR(V,N)))
;deps: (EXT1)

(trw |nthcdr(v,length u)| (use ext1 last_nthcdr mode: exact))
;NTHCDR(V,LENGTH U)=NIL

(ue  ((phi4.|λu n.(∀i.i<length u⊃appl(u,i)=appl(nthcdr(v,n),i))⊃u=nthcdr(v,n)|)
      (u.u)) nthcdr_induction1 (open appl) * -2)
;(∀I.I<LENGTH U⊃NTH(U,I)=NTH(V,I))⊃U=V

(ci ext1)
;LENGTH U=LENGTH V⊃((∀I.I<LENGTH U⊃NTH(U,I)=NTH(V,I))⊃U=V)

(derive |∀u v.length u=length v∧(∀i.i<length u⊃appl(u,i)=appl(v,i))⊃u=v| *)

;applfact has been proved already for nth

(trw |∀u i.i<length u ⊃ sexp(appl(u,i))∧member(appl(u,i),u)| (open appl) nthmember)
;∀U I.I<LENGTH U⊃SEXP APPL(U,I)∧MEMBER(APPL(U,I),U)

;equivalence of uniqueness and inj
(proof uniqueness_inj)

(ue (phi3 |λu n.uniqueness u⊃uniqueness nthcdr(u,n)|) doubleinduction1
        (open uniqueness nthcdr))
;∀U N.UNIQUENESS(U)⊃UNIQUENESS(NTHCDR(U,N))
(label uniqueness_nthcdr)

(assume |uniqueness(u)|)
(label ui1)

(assume |i<length u|)
(label ui2)

(assume |j<length u|)
(label ui3)

(assume |nth(u,i)=nth(u,j)|)
(label ui4)

(derive |uniqueness(nthcdr(u,i))|(uniqueness_nthcdr ui1))

(rw * (use nthcdr_car_cdr ui2 mode: always) (open uniqueness))
;¬MEMBER(NTH(U,I),NTHCDR(U,I'))∧UNIQUENESS(NTHCDR(U,I'))
;deps: (UI1 UI2)

;labels: NTH_IN_NTHCDR 
;∀U N M.N≤M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N))

(ue ((u.u)(n.|i'|)(m.j)) nth_in_nthcdr 
    (use ui4 mode: exact direction: reverse) 
    (use ui3 * mode: exact))
;¬I'≤J
;deps: (UI1 UI2 UI3 UI4)

;labels: LESS_LESSEQSUCC 
;∀M N.M<N=M'≤N

(ue ((m.i)(n.j)) less_lesseqsucc *)
;¬I<J
(label ui_way1)
;deps: (UI1 UI2 UI3 UI4)

(ci (ui1 ui2 ui3 ui4))
;UNIQUENESS(U)∧I<LENGTH U∧J<LENGTH U∧NTH(U,I)=NTH(U,J)⊃¬I<J

(ue ((i.j)(j.i)) *)
;UNIQUENESS(U)∧J<LENGTH U∧I<LENGTH U∧NTH(U,J)=NTH(U,I)⊃¬J<I

(derive |¬j<i| (* ui1 ui2 ui3 ui4))
(label ui_way2)
;deps: (UI1 UI2 UI3 UI4)

(derive |i=j| (trichotomy ui_way1 ui_way2))
;deps: (UI1 UI2 UI3 UI4)

(ci (ui1 ui2 ui3 ui4))
;UNIQUENESS(U)∧I<LENGTH U∧J<LENGTH U∧NTH(U,I)=NTH(U,J)⊃I=J

(trw |uniqueness(u)⊃inj(u)| * (open inj))
;UNIQUENESS(U)⊃INJ(U)
;equivalence of uniqueness and inj
(proof inj_uniqueness)

(assume |inj u|)(label iu1)
(rw * (open inj))
;∀N M.N<LENGTH U∧M<LENGTH U∧NTH(U,N)=NTH(U,M)⊃N=M
(label iu2)

(assume |member(nth(u,n),nthcdr(u,n'))|)(label iu3)

(assume |length(u)≤n'|)(label iu4)
(rw iu3 (use trivial_nthcdr iu4 mode: always) (open member))
;FALSE
;deps: (IU3 iu4)
(ci iu4)
;¬LENGTH U≤N'
;deps: (IU3)

(derive |n'<length u| (* trichotomy2))
(label iu6)

;we use:
;labels: MEMBER_NTH 
;∀U Y.MEMBER(Y,U)⊃(∃N.N<LENGTH U∧NTH(U,N)=Y)

(ue ((u.|nthcdr(u,n')|)(y.|nth(u,n)|)) member_nth iu3)
;∃N1.N1<LENGTH (NTHCDR(U,N'))∧NTH(NTHCDR(U,N'),N1)=NTH(U,N)
(label iu7)

(define mv |mv<length(nthcdr(u,n'))∧nth(nthcdr(u,n'),mv)=nth(u,n)| *)
(label iu8)

;we use:
;labels: NTH_NTHCDR 
;∀U N M.N<LENGTH U∧M<LENGTH (NTHCDR(U,N))⊃
;          NTH(NTHCDR(U,N),M)=NTH(U,M+N)

(ue ((u.u)(n.|n'|)(m.mv)) nth_nthcdr (iu8 iu6))
;NTH(U,N)=NTH(U,(MV+N)')
(label iu9)

(ue ((u.u)(n.|n'|)) length_nthcdr iu6 (open lesseq))
;LENGTH (NTHCDR(U,N'))=LENGTH U-N'

(derive |mv<length u-n'| (iu8 *))

(ue ((n.|length u|)(k.|n'|)(m.mv)) inequality_law * iu6)
;(MV+N)'<LENGTH U
(label iu10)

(derive |n=(mv+n)'| (iu2 iu6 succ_less_less iu9 iu10))

(ue (a |λn.n≠m+n'|) proof_by_induction)
;∀N.¬N=(M+N)'

(rw -2 *)
;FALSE
;deps: (IU1 IU3)

(ci iu3)
;¬MEMBER(NTH(U,N),NTHCDR(U,N'))
;deps: (IU1)

(ue ((phi.|λu.uniqueness u|)(u.u)) nthcdr_induction (open uniqueness) *)
;UNIQUENESS(U)
;deps: (IU1)

(ci IU1)
;INJ(U)⊃UNIQUENESS(U)
;unpleasant rewriting
(proof unpleasant)

(show lispax#24)
;labels: SIMPINFO 
;(AXIOM |∀X Y.CAR (X.Y)=X|)

(show lispax#25)
;labels: SIMPINFO 
25. (AXIOM |∀X Y.CDR (X.Y)=Y|)

(trw |x.z=xa.y⊃car(x.z)=car(xa.y)∧cdr(x.z)=cdr(xa.y)| (nuse lispax#24 lispax#25))
;X.Z=XA.Y⊃CAR (X.Z)=CAR (XA.Y)∧CDR (X.Z)=CDR (XA.Y)

(rw *)
;X.Z=XA.Y⊃X=XA∧Z=Y
;alist induction
(proof alistind)

(assume |chi(nil)∧(∀xa y alist.chi(alist)⊃chi((xa.y).alist))|)(label alind1)
(assume |alistp u⊃chi u|)(label alind2)
(assume |alistp (x.u)|)(label alind3)
(ue (alist |x.u|) alistdef *)
;¬ATOM X∧ATOM CAR X∧ALISTP U

(derive |(∀xa y alist.chi(alist)⊃chi((xa.y).alist))| alind1)

(ue ((xa.|car x|)(y.|cdr(x)|)(alist.u)) * -2 alind3 alind2)
;CHI(X.U)
;deps: (ALIND1 ALIND2 ALIND3)

(ci alind3)
;ALISTP X.U⊃CHI(X.U)
;deps: (ALIND1 ALIND2)

(ci alind2)
;(ALISTP U⊃CHI(U))⊃(ALISTP X.U⊃CHI(X.U))
;deps: (ALIND1)

(ue (phi |λu.alistp(u)⊃chi(u)|) listinduction * alind1)
;∀U.ALISTP U⊃CHI(U)

(derive |∀alist.chi alist| *)
;deps: (ALIND1)

(ci alind1)
;CHI(NIL)∧(∀XA Y ALIST.CHI(ALIST)⊃CHI((XA.Y).ALIST))⊃(∀ALIST.CHI(ALIST))
(proof alistproofs)
(unlabel simpinfo domsort rangesort appalistsort)
;domsort

(ue (chi |λalist.listp dom(alist)|) alistinduction (open dom))
;∀ALIST.LISTP DOM(ALIST)
(label simpinfo domsort)

;rangesort

(ue (chi |λalist.listp range(alist)|) alistinduction (open range))
;∀ALIST.LISTP RANGE(ALIST)
(label simpinfo rangesort)

;domlength

(ue (chi |λalist.length dom alist=length alist|) alistinduction (open dom))
;∀ALIST.LENGTH (DOM(ALIST))=LENGTH ALIST

;domrangelength 

(ue (chi |λalist.length(dom alist)=length(range alist)|) alistinduction (open dom range))
;∀ALIST.LENGTH (DOM(ALIST))=LENGTH (RANGE(ALIST))

;appalistsort

(ue (chi |λalist.sexp appalist(y,alist)|) alistinduction (part 1(open appalist assoc)))
;∀ALIST.SEXP APPALIST(Y,ALIST)
(label simpinfo appalistsort)

;trivial appalist

(ue (chi |λalist.¬(yεmklset dom(alist))⊃appalist(y,alist)=nil|) alistinduction
    (part 1 (open epsilon mklset dom appalist assoc member)))
;∀ALIST.¬YεMKLSET(DOM(ALIST))⊃APPALIST(Y,ALIST)=NIL

;member range

(ue (chi |λalist.member(z,range alist)⊃(∃x.member(x.z,alist))|)
         alistinduction 
   (open range member)(use normal mode: always))
;∀ALIST.MEMBER(Z,RANGE(ALIST))⊃(∃X.MEMBER(X.Z,ALIST))

;membership alist range

(trw |∀x y.x=y⊃cdr x=cdr y|)
;∀X Y.X=Y⊃CDR X=CDR Y

(ue ((x.|x.z|)(y.|xa.y|)) *)
;X.Z=XA.Y⊃Z=Y

(ue (chi |λalist.member(x.z,alist)⊃member(z,range alist)|)
          alistinduction
     (open appalist assoc range member)
   (use demorgan1 * normal mode: always))
;∀ALIST.MEMBER(X.Z,ALIST)⊃MEMBER(Z,RANGE(ALIST))

;trivial assoc

;(ue (chi |λalist.x=cdr assoc(z,alist)∧atom assoc(z,alist)⊃null x|) alistinduction
;    (open assoc))
;∀ALIST.X=CDR ASSOC(Z,ALIST)∧ATOM ASSOC(Z,ALIST)⊃NULL X
;samemap

(trw |samemap(alist,alist)|(open samemap))
;SAMEMAP(ALIST,ALIST)

(trw |samemap(alist,alist1)⊃samemap(alist1,alist)| (open samemap mklset dom))
;SAMEMAP(ALIST,ALIST1)⊃SAMEMAP(ALIST1,ALIST)

(trw |samemap(alist,alist1)∧samemap(alist1,alist2)⊃samemap(alist,alist2)|
    (open samemap mklset dom))
;SAMEMAP(ALIST,ALIST1)∧SAMEMAP(ALIST1,ALIST2)⊃SAMEMAP(ALIST,ALIST2)

;apparently stronger definition of samemap

(proof samemap)

(trw
    |∀alist1 alist2.mklset dom(alist1)=mklset dom(alist2)⊃
                    (∀y.¬yεmklset(dom(alist1))⊃
                        appalist(y,alist1)=appalist(y,alist2))|
    (use trivial_appalist mode: always))
;∀ALIST1 ALIST2.MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))⊃
;               (∀Y.¬YεMKLSET(DOM(ALIST1))⊃
;                   APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2))
(label trivial_samemap)

(assume |samemap(alist1,alist2)|)
(rw * (open samemap))
;MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧
;(∀Y.YεMKLSET(DOM(ALIST1))⊃APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2))

(derive |∀y.¬yεmklset(dom(alist1))⊃appalist(y,alist1)=appalist(y,alist2)|
        (trivial_samemap *))

(ue ((a.|λy.yεmklset dom(alist1)|)(b.|λy.appalist(y,alist1)=appalist(y,alist2)|))
    disjunctive_syllogism -2 *)
;∀X.APPALIST(X,ALIST1)=APPALIST(X,ALIST2)

(derive |mklset dom(alist1)=mklset dom(alist2)∧
         ∀x.appalist(x,alist1)=appalist(x,alist2)| (-3 *))
         
(ci -5)
;SAMEMAP(ALIST1,ALIST2)⊃
;MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧
;(∀X.APPALIST(X,ALIST1)=APPALIST(X,ALIST2))

(derive |SAMEMAP(ALIST1,ALIST2)≡
        (MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧
        (∀X.APPALIST(X,ALIST1)=APPALIST(X,ALIST2)))| *)